:- dynamic fullyProjectedPred/2.
:- dynamic projectionRule/2.

evaluate(H,B) :-
	call(B),
	addFact(H),
	fail.
evaluate(_, _).

%%  projection has a single subgoal as either body or head
clearBody(B) :-
	functor(B,F,N),
	removeAllFacts(F,N).

contract :-
	dynoProjRules,
	abolishFullyProjected,
	contractAll,
	clearFullyProjected.

dynoProjRules :-
	projectionRule(H, B),
	dyno(H),
	dyno(B),
	fail.
dynoProjRules.

contractAll :-
	projectionRule(H, B),
	contract(H,B),
	fail.
contractAll .

%% contract(H, B) :- evaluate_clear(H, B), inverse((H, B), (NH, NB)), evaluate_clear(NH, NB).

%% new contraction without introducing long skolems
contract(H, B) :-
	evaluate_clear(H, B),
	expand_clear(H, B).


expand(H, B) :-
	call(H),
	genTuples(B),
	fail.
expand(_, _).

expand_clear(H, B) :-
	expand(H, B),
	clearBody(H).

evaluate_clear(H, B) :-
	evaluate(H, B),
	clearBody(B).

project_signature :-
	dynamicalize,
	abolishFullyProjected,
	evaluate_clear_all,
	clearFullyProjected.

evaluate_clear_all :-
	projectionRule(H,B),
	evaluate_clear(H,B),
	fail.
evaluate_clear_all.

inverse((H,B), (NH, NB)) :-
	skolemize((B, H), (NH,NB,_)).

tellProjectionRule('<-'(H,B)) :-
	skolemize((H,B), (NH, NB, OH)),
	assert(projectionRule(NH, NB)).
tellProjectionRule('->'(B,H)) :-
	tellProjectionRule('<-'(H, B)).
tellProjectionRule('<->'(H,B)) :-
	tellProjectionRule('<-'(H,B)),
	tellProjectionRule('->'(H,B)).

clearProjectionRules :-
	retractall(projectionRule(_, _)).

abolishFullyProjected :-
	fullyProjectedPred(Pred, N),
	removeAllFacts(Pred, N),
	fail.
abolishFullyProjected .

tellFullyProjected(Pred, N) :-
	assert(fullyProjectedPred(Pred, N)).
clearFullyProjected :-
	retractall(fullyProjectedPred(_,_)).
